Search Results

Documents authored by de'Liguoro, Ugo

Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2020
LIPIcs, Volume 188, TYPES 2020, Complete Volume

Authors: Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract
LIPIcs, Volume 188, TYPES 2020, Complete Volume
Cite as

26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 1-204, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Proceedings{deliguoro_et_al:LIPIcs.TYPES.2020,
  title =	{{LIPIcs, Volume 188, TYPES 2020, Complete Volume}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{1--204},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020},
  URN =		{urn:nbn:de:0030-drops-138785},
  doi =		{10.4230/LIPIcs.TYPES.2020},
  annote =	{Keywords: LIPIcs, Volume 188, TYPES 2020, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2020.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{deliguoro_et_al:LIPIcs.TYPES.2020.0,
  author =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{0:i--0:viii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.0},
  URN =		{urn:nbn:de:0030-drops-138792},
  doi =		{10.4230/LIPIcs.TYPES.2020.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.15
Mailbox Types for Unordered Interactions

Authors: Ugo de'Liguoro and Luca Padovani

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
We propose a type system for reasoning on protocol conformance and deadlock freedom in networks of processes that communicate through unordered mailboxes. We model these networks in the mailbox calculus, a mild extension of the asynchronous pi-calculus with first-class mailboxes and selective input. The calculus subsumes the actor model and allows us to analyze networks with dynamic topologies and varying number of processes possibly mixing different concurrency abstractions. Well-typed processes are deadlock free and never fail because of unexpected messages. For a non-trivial class of them, junk freedom is also guaranteed. We illustrate the expressiveness of the calculus and of the type system by encoding instances of non-uniform, concurrent objects, binary sessions extended with joins and forks, and some known actor benchmarks.
Cite as

Ugo de'Liguoro and Luca Padovani. Mailbox Types for Unordered Interactions. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 15:1-15:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{deliguoro_et_al:LIPIcs.ECOOP.2018.15,
  author =	{de'Liguoro, Ugo and Padovani, Luca},
  title =	{{Mailbox Types for Unordered Interactions}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{15:1--15:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.15},
  URN =		{urn:nbn:de:0030-drops-92209},
  doi =		{10.4230/LIPIcs.ECOOP.2018.15},
  annote =	{Keywords: actors, concurrent objects, first-class mailboxes, unordered communication protocols, behavioral types, protocol conformance, deadlock freedom, junk freedom}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.77
Knowledge Spaces and the Completeness of Learning Strategies

Authors: Stefano Berardi and Ugo de'Liguoro

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
We propose a theory of learning aimed to formalize some ideas underlying Coquand's game semantics and Krivine's realizability of classical logic. We introduce a notion of knowledge state together with a new topology, capturing finite positive and negative information that guides a learning strategy. We use a leading example to illustrate how non-constructive proofs lead to continuous and effective learning strategies over knowledge spaces, and prove that our learning semantics is sound and complete w.r.t. classical truth, as it is the case for Coquand's and Krivine's approaches.
Cite as

Stefano Berardi and Ugo de'Liguoro. Knowledge Spaces and the Completeness of Learning Strategies. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 77-91, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{berardi_et_al:LIPIcs.CSL.2012.77,
  author =	{Berardi, Stefano and de'Liguoro, Ugo},
  title =	{{Knowledge Spaces and the Completeness of Learning Strategies}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{77--91},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.77},
  URN =		{urn:nbn:de:0030-drops-36656},
  doi =		{10.4230/LIPIcs.CSL.2012.77},
  annote =	{Keywords: Classical Logic, Proof Mining, Game Semantics, Learning, Realizability}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact